Validating or verifying computer software is a common concern among software developers and users. Whether a piece of software is, for example, a desktop application for installation and execution at one or more client computer systems or a web application for execution at one or more server computer systems, it is often important to carefully verify the quality of the software in order to ensure that it functions correctly. While some types of errors in software, such as bugs, cause annoyance or inconvenience to software users, other types of errors in software have the potential of causing more serious problems, possibly even resulting in significant financial losses to institutions.
Software testing is a common method of verifying the quality of software. With software testing, the software or one or more portions of the software under analysis is/are put through a suite of regression tests after each revision or modification and the outputs are evaluated for correctness. However, software testing often provides only limited coverage and has a tendency to miss corner-case bugs. Formal verification tends to address these problems. Formal verification mathematically proves the satisfiability of a specific requirement on the software under analysis or obtains a counter-example in the form of a test case that breaks the requirement and thus indicates a bug.
A software application may include any number of modules, and each module may be tested or validated individually or multiple modules may be tested or validated in combination. A software module may be tested or validated manually or automatically. In the former case, a person (e.g., a software testing engineer) may manually design test cases for the software module based on the design specification of the module, execute the module under the test cases, and check for module behavior or output that does not agree with the test cases. In the later case, a software testing tool, implemented as computer software or hardware, may automatically generate test cases for a software module under analysis, execute the module while simulating the test cases, and check for module behavior or output that does not agree with the test cases.